Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    a(f,0)  → a(s,0)
2:    a(d,0)  → 0
3:    a(d,a(s,x))  → a(s,a(s,a(d,a(p,a(s,x)))))
4:    a(f,a(s,x))  → a(d,a(f,a(p,a(s,x))))
5:    a(p,a(s,x))  → x
There are 8 dependency pairs:
6:    A(f,0)  → A(s,0)
7:    A(d,a(s,x))  → A(s,a(s,a(d,a(p,a(s,x)))))
8:    A(d,a(s,x))  → A(s,a(d,a(p,a(s,x))))
9:    A(d,a(s,x))  → A(d,a(p,a(s,x)))
10:    A(d,a(s,x))  → A(p,a(s,x))
11:    A(f,a(s,x))  → A(d,a(f,a(p,a(s,x))))
12:    A(f,a(s,x))  → A(f,a(p,a(s,x)))
13:    A(f,a(s,x))  → A(p,a(s,x))
The approximated dependency graph contains 2 SCCs: {9} and {12}.
Tyrolean Termination Tool  (0.02 seconds)   ---  May 3, 2006